Nuprl Definition : list_accum
11,40
postcript
pdf
list_accum(
x
,
a
.
f
(
x
;
a
);
y
;
l
)
== rec-case(
l
) of [] =>
y
|
b
::
l'
=>
.list_accum(
x
,
a
.
f
(
x
;
a
);
f
(
y
;
b
);
l'
)
(recursive)
latex
Definitions
Y
,
x
.
A
(
x
)
,
rec-case(
a
) of [] =>
s
|
x
::
y
=>
z
.
t
(
x
;
y
;
z
)
,
f
(
a
)
FDL editor aliases
list_accum
origin
x.A(x)x.A(x)